<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Tag</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}

\usepackage[references]{agda}

\begin{document}

</a><a id="75" class="Markup">\begin{code}</a>
<a id="88" class="Keyword">module</a> <a id="95" href="Tag.html" class="Module">Tag</a> <a id="99" class="Keyword">where</a>

<a id="106" class="Keyword">module</a> <a id="Apa"></a><a id="113" href="Tag.html#113" class="Module">Apa</a> <a id="117" class="Keyword">where</a>

<a id="bepa"></a><a id="124" href="Tag.html#124" class="Function">bepa</a> <a id="129" class="Symbol">:</a> <a id="131" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="135" class="Symbol">→</a> <a id="137" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="141" href="Tag.html#124" class="Function">bepa</a> <a id="146" href="Tag.html#146" class="Bound">x</a> <a id="148" class="Symbol">=</a> <a id="150" href="Tag.html#146" class="Bound">x</a>

<a id="153" class="Keyword">data</a> <a id="Cepa"></a><a id="158" href="Tag.html#158" class="Datatype">Cepa</a> <a id="163" class="Symbol">:</a> <a id="165" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="169" class="Keyword">where</a>
  <a id="Cepa.cepa"></a><a id="177" href="Tag.html#177" class="InductiveConstructor">cepa</a> <a id="182" class="Symbol">:</a> <a id="184" href="Tag.html#158" class="Datatype">Cepa</a>

<a id="190" class="Keyword">record</a> <a id="Depa"></a><a id="197" href="Tag.html#197" class="Record">Depa</a> <a id="202" class="Symbol">:</a> <a id="204" href="Agda.Primitive.html#311" class="Primitive">Set₁</a> <a id="209" class="Keyword">where</a>
  <a id="217" class="Keyword">field</a>
    <a id="Depa.depa"></a><a id="227" href="Tag.html#227" class="Field">depa</a> <a id="232" class="Symbol">:</a> <a id="234" href="Agda.Primitive.html#311" class="Primitive">Set</a>

<a id="239" class="Keyword">postulate</a>
  <a id="epa"></a><a id="251" href="Tag.html#251" class="Postulate">epa</a> <a id="255" class="Symbol">:</a> <a id="257" href="Agda.Primitive.html#311" class="Primitive">Set</a>

<a id="262" class="Keyword">postulate</a>
  <a id="α"></a><a id="274" href="Tag.html#274" class="Postulate">α</a>   <a id="278" class="Symbol">:</a> <a id="280" href="Agda.Primitive.html#311" class="Primitive">Set</a>
  <a id="_∘_"></a><a id="286" href="Tag.html#286" class="Postulate Operator">_∘_</a> <a id="290" class="Symbol">:</a> <a id="292" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="296" class="Markup">\end{code}</a><a id="306" class="Background">

\begin{tabular}{ll}
  Name &amp; Test \\
  \hline
  Apa   &amp; \AgdaRef{Apa} \\
  bepa  &amp; \AgdaRef{bepa} \\
  Cepa  &amp; \AgdaRef{Cepa} \\
  cepa  &amp; \AgdaRef{cepa} \\
  Depa  &amp; \AgdaRef{Depa} \\
  depa  &amp; \AgdaRef{depa} \\
  epa   &amp; \AgdaRef{epa} \\
  α     &amp; \AgdaRef{α} \\
  \_∘\_ &amp; \AgdaRef{\_∘\_} \\
\end{tabular}

\end{document}
</a></pre></body></html>